Nuprl Lemma : branch_wf2
11,40
postcript
pdf
P
:
,
d
:Dec(
P
),
T
:Type,
A
:(
P
T
),
B
:(
q
:
P
.
T
). if
p
:
P
then
A
(
p
) else
B
fi
T
latex
ProofTree
Definitions
A
,
x
:
A
.
B
(
x
)
,
t
T
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
,
Dec(
P
)
,
left
+
right
,
Void
,
P
Q
,
False
,
case
b
of inl(
x
) =>
s
(
x
) | inr(
y
) =>
t
(
y
)
,
Type
,
if
p
:
P
then
A
(
p
) else
B
fi
,
P
Q
origin
P:
, d:Dec(P), T:Type, A:(P
T), B:(
q:
P.T). if p:P then A(p) else B fi 
T
P:, d:Dec(P), T:Type, A:(PT), B:(q:P.T). if p:P then A(p) else B fi T
Ax:A.B(x) TB(x)x:A. B(x)
Q
Q